Issue5434-3.agda:6,5-6
(@0 A : Set) → A → D A is not usable at the required modality
when checking that the type (@0 A : Set) → A → D A of the
constructor c fits in the sort Set₁ of the datatype.
